/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BASB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH25/FONT#8=FIX25



␈↓ α∧␈↓αEXTENSIONAL FORMS

␈↓ α∧␈↓␈↓ αTConsider␈α∂first␈α∂ordinary␈α∂forms,␈α∂i.e.␈α∞expressions␈α∂built␈α∂from␈α∂symbols␈α∂for␈α∂constants,␈α∞variables
␈↓ α∧␈↓and␈αfunctions␈αand␈αpossibly␈αquantifiers␈αand␈αthe␈αChurch␈αlambda␈αoperator.␈α Such␈αa␈αform␈αwill␈αhave
␈↓ α∧␈↓certain␈αfree␈αvariables,␈αand␈αits␈αvalue␈αwill␈αdepend␈αon␈αthe␈αvalues␈αassigned␈αto␈αthe␈αfree␈αvariables.␈α We
␈↓ α∧␈↓call␈α
two␈αforms␈α
␈↓↓extensionally␈↓␈α␈↓↓equivalent␈↓␈α
if␈αthey␈α
have␈α
the␈αsame␈α
value␈αfor␈α
all␈αassignments␈α
of␈αvalues␈α
to
␈↓ α∧␈↓the␈αfree␈αvariables␈α
they␈αcontain.␈α Thus␈α
if␈α+␈αhas␈α
its␈αusual␈αinterpretation␈α
on␈αthe␈αintegers,␈α
the␈αforms
␈↓ α∧␈↓␈↓↓x+y␈↓␈αand␈α␈↓↓y+x␈↓␈αare␈αextensionally␈αequivalent,␈αbut␈αneither␈αof␈αthem␈αis␈αextensionally␈αequivalent␈αto␈α␈↓↓u+v,␈↓
␈↓ α∧␈↓because assigning ␈↓↓x␈↓ and ␈↓↓y␈↓ the value 0 and ␈↓↓u␈↓ and ␈↓↓v␈↓ the value 1 gives the forms different values.

␈↓ α∧␈↓␈↓ αTExtensional␈α∞forms␈α
can␈α∞be␈α
regarded␈α∞as␈α
the␈α∞equivalence␈α
classes␈α∞of␈α
this␈α∞equivalence␈α
relation,
␈↓ α∧␈↓but␈α∩instead␈α∩of␈α∩first␈α⊃introducing␈α∩ordinary␈α∩forms␈α∩and␈α⊃the␈α∩equivalence␈α∩relation,␈α∩we␈α∩will␈α⊃define
␈↓ α∧␈↓extensional␈α
forms␈α
inductively␈α
from␈α
the␈α
symbols␈αfor␈α
constants,␈α
variables,␈α
and␈α
functions.␈α
 In␈αorder␈α
to
␈↓ α∧␈↓motivate␈α⊃the␈α⊃reader's␈α⊂attention␈α⊃to␈α⊃a␈α⊂somewhat␈α⊃boring␈α⊃inductive␈α⊂definition,␈α⊃we␈α⊃remark␈α⊃on␈α⊂the
␈↓ α∧␈↓following␈α∞virtues␈α
of␈α∞extensional␈α
forms:␈α∞First␈α
they␈α∞have␈α
no␈α∞bound␈α
variables␈α∞which␈α∞simplifies␈α
the
␈↓ α∧␈↓statement␈α
of␈α
the␈αlaws␈α
of␈α
substitution,␈αand␈α
second␈α
all␈αthe␈α
ways␈α
of␈αbuilding␈α
up␈α
extensional␈αforms␈α
are
␈↓ α∧␈↓by␈α∪the␈α∪application␈α∪of␈α∪functions␈α∩to␈α∪constituent␈α∪forms;␈α∪even␈α∪␈↓↓λ(x,e)␈↓␈α∩is␈α∪just␈α∪a␈α∪function␈α∪of␈α∩two
␈↓ α∧␈↓extensional␈α∞forms␈α
␈↓↓x␈↓␈α∞and␈α∞␈↓↓e.␈↓␈α
Consequently␈α∞the␈α∞syntax␈α
and␈α∞semantics␈α∞of␈α
extensional␈α∞forms␈α∞can␈α
be
␈↓ α∧␈↓axiomatized␈αin␈αfirst␈αorder␈αlogic.␈α This␈αis␈αimportant␈αfor␈αthe␈αapplications␈αto␈αmathematical␈αtheory␈αof
␈↓ α∧␈↓computation and to the theory of concepts.

␈↓ α∧␈↓␈↓ αTWe start with a simplified theory:

␈↓ α∧␈↓␈↓ αTLet␈α␈↓↓D␈↓␈αbe␈αa␈αdomain,␈αe.g.␈αthe␈αintegers␈αor␈αpeople␈αor␈αconcepts␈αof␈αintegers␈αor␈αconcepts␈αof␈αpeople.
␈↓ α∧␈↓Let␈α␈↓↓V␈↓␈α
be␈αan␈α
infinite␈αclass␈α
of␈αobjects␈α
called␈αvariables,␈αand␈α
let␈α␈↓↓E␈↓␈α
be␈αanother␈α
class␈αof␈α
objects␈αcalled
␈↓ α∧␈↓environments.␈α∂ Let␈α∞␈↓↓value:␈α∂V␈α∞␈↓πx␈↓↓␈α∂E␈α∞→␈α∂D␈↓␈α∂be␈α∞a␈α∂distinguished␈α∞function.␈α∂ We␈α∞will␈α∂call␈α∂␈↓↓value(x,e)␈↓␈α∞the
␈↓ α∧␈↓value␈α∪of␈α∪the␈α∪variable␈α∪␈↓↓x␈α∩in␈↓␈α∪the␈α∪environment␈α∪␈↓↓e.␈↓␈α∪We␈α∩assume␈α∪an␈α∪axiom␈α∪of␈α∪extensionality␈α∩for
␈↓ α∧␈↓environments, namely

␈↓ α∧␈↓Ext1)␈↓ αt ␈↓↓∀e1 e2.(∀x.(value(x,e1) = value(x,e2)) ⊃ e1 = e2)␈↓.

␈↓ α∧␈↓Ext1␈αimplies␈αthat␈αenvironments␈αcan␈αbe␈αidentified␈αwith␈αcertain␈αfunctions␈αfrom␈αvariables␈αto␈αdomain
␈↓ α∧␈↓elements.  However, we cannot conclude that all such functions are represented by environments.

␈↓ α∧␈↓␈↓ αTNext we have the assignment function ␈↓↓assign: V ␈↓πx␈↓↓ D ␈↓πx␈↓↓ E → E␈↓.  It satisfies the axioms

␈↓ α∧␈↓Ext2)␈↓ αt ␈↓↓∀x d e.(value(x,assign(x,d,e)) = d)␈↓

␈↓ α∧␈↓and

␈↓ α∧␈↓Ext3)␈↓ αt ␈↓↓∀x y d e.(y≠x ⊃ value(y,assign(x,d,e)) = value(y,e))␈↓.








␈↓ α∧␈↓␈↓ ε|1␈↓ ∧